Experiments with an Agent-Oriented Reasoning System
Identifieur interne : 000C93 ( Main/Exploration ); précédent : 000C92; suivant : 000C94Experiments with an Agent-Oriented Reasoning System
Auteurs : Christoph Benzmüller [Allemagne] ; Manfred Kerber [Royaume-Uni] ; Mateja Jamnik [Royaume-Uni] ; Volker Sorge [Allemagne]Source :
- Lecture Notes in Computer Science [ 0302-9743 ] ; 2001.
English descriptors
- Teeft :
- Abstract inferences, Agent paradigm, Algebra, Algebra examples, Available resources, Backtrack store, Backtracking, Backtracking information, Backtracking purposes, Broker, Calculus, Central proof object, Centralised approach, Computer algebra system maple, Computer algebra systems, Concrete examples, Core system, Current proof context, Deduction calculus, Deduction proof object, Deduction systems, Description operator, Domain tactics, Exible, Extensionality reasoning, External reasoners, External reasoning systems, External system, External systems, Future work, Graphical user interface loui, Group theory, Heterogeneous systems, Heuristic, Heuristic criteria, Interactive, Knowledge sources, Large proofs, Lnai, Logic broker architecture, Logical issues, Loui, Maple service, Mathweb, Model generator, Natural deduction layer, Natural deduction proof search, Natural deduction rules, Natural deduction style, Oants, Open approach, Partial proof, Partial proofs, Partial result, Partial results, Particular niches, Particular parameter instantiations, Problem classes, Proc, Promising direction, Proof data structure, Proof object, Proof search, Proof step, Propositional, Propositional logic prover, Prover, Provers, Reactive, Reactive layer, Reactive suggestion layer, Reactive suggestion mechanism, Reasoner, Reasoning, Reasoning agents, Reasoning system, Reasoning systems, Rstorder clauses, Search space, Simple examples, Skeptical approach, Skolem variables, Specialised, Specialised reasoning systems, Springer, Subgoal, Symbolic computation, System architecture, Theorem prover, Theorem provers, Transformation tools, Unique element, Unit element, User, User interaction.
Abstract
Abstract: This paper discusses experiments with an agent oriented approach to automated and interactive reasoning. The approach combines ideas from two subfields of AI (theorem proving/proof planning and multi-agent systems) and makes use of state of the art distribution techniques to decentralise and spread its reasoning agents over the internet. It particularly supports cooperative proofs between reasoning systems which are strong in different application areas, e.g., higher-order and first-order theorem provers and computer algebra systems
Url:
DOI: 10.1007/3-540-45422-5_29
Affiliations:
- Allemagne, Royaume-Uni
- Angleterre, Midlands de l'Ouest, Sarre (Land)
- Birmingham, Sarrebruck
- Université de Birmingham
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: 001117
- to stream Istex, to step Curation: 001034
- to stream Istex, to step Checkpoint: 000A84
- to stream Main, to step Merge: 000C94
- to stream Main, to step Curation: 000C93
Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct:series"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Experiments with an Agent-Oriented Reasoning System</title><author><name sortKey="Benzmuller, Christoph" sort="Benzmuller, Christoph" uniqKey="Benzmuller C" first="Christoph" last="Benzmüller">Christoph Benzmüller</name></author><author><name sortKey="Kerber, Manfred" sort="Kerber, Manfred" uniqKey="Kerber M" first="Manfred" last="Kerber">Manfred Kerber</name></author><author><name sortKey="Jamnik, Mateja" sort="Jamnik, Mateja" uniqKey="Jamnik M" first="Mateja" last="Jamnik">Mateja Jamnik</name></author><author><name sortKey="Sorge, Volker" sort="Sorge, Volker" uniqKey="Sorge V" first="Volker" last="Sorge">Volker Sorge</name></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:A40A289851FC6A763117E357C28D52A49E98E8ED</idno><date when="2001" year="2001">2001</date><idno type="doi">10.1007/3-540-45422-5_29</idno><idno type="url">https://api.istex.fr/document/A40A289851FC6A763117E357C28D52A49E98E8ED/fulltext/pdf</idno><idno type="wicri:Area/Istex/Corpus">001117</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">001117</idno><idno type="wicri:Area/Istex/Curation">001034</idno><idno type="wicri:Area/Istex/Checkpoint">000A84</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">000A84</idno><idno type="wicri:doubleKey">0302-9743:2001:Benzmuller C:experiments:with:an</idno><idno type="wicri:Area/Main/Merge">000C94</idno><idno type="wicri:Area/Main/Curation">000C93</idno><idno type="wicri:Area/Main/Exploration">000C93</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Experiments with an Agent-Oriented Reasoning System</title><author><name sortKey="Benzmuller, Christoph" sort="Benzmuller, Christoph" uniqKey="Benzmuller C" first="Christoph" last="Benzmüller">Christoph Benzmüller</name><affiliation wicri:level="3"><country xml:lang="fr">Allemagne</country><wicri:regionArea>Fachbereich Informatik, Universität des Saarlandes, 66041, Saarbrücken</wicri:regionArea><placeName><region type="land" nuts="2">Sarre (Land)</region><settlement type="city">Sarrebruck</settlement></placeName></affiliation><affiliation wicri:level="1"><country wicri:rule="url">Allemagne</country></affiliation></author><author><name sortKey="Kerber, Manfred" sort="Kerber, Manfred" uniqKey="Kerber M" first="Manfred" last="Kerber">Manfred Kerber</name><affiliation wicri:level="4"><country xml:lang="fr">Royaume-Uni</country><wicri:regionArea>School of Computer Science, The University of Birmingham, Birmingham B15 2TT, England</wicri:regionArea><orgName type="university">Université de Birmingham</orgName><placeName><settlement type="city">Birmingham</settlement><region type="country">Angleterre</region><region type="région" nuts="1">Midlands de l'Ouest</region></placeName></affiliation><affiliation wicri:level="1"><country wicri:rule="url">Royaume-Uni</country></affiliation></author><author><name sortKey="Jamnik, Mateja" sort="Jamnik, Mateja" uniqKey="Jamnik M" first="Mateja" last="Jamnik">Mateja Jamnik</name><affiliation wicri:level="1"><country wicri:rule="url">Royaume-Uni</country></affiliation></author><author><name sortKey="Sorge, Volker" sort="Sorge, Volker" uniqKey="Sorge V" first="Volker" last="Sorge">Volker Sorge</name><affiliation wicri:level="3"><country xml:lang="fr">Allemagne</country><wicri:regionArea>Fachbereich Informatik, Universität des Saarlandes, 66041, Saarbrücken</wicri:regionArea><placeName><region type="land" nuts="2">Sarre (Land)</region><settlement type="city">Sarrebruck</settlement></placeName></affiliation><affiliation wicri:level="1"><country wicri:rule="url">Allemagne</country></affiliation></author></analytic><monogr></monogr><series><title level="s">Lecture Notes in Computer Science</title><imprint><date>2001</date></imprint><idno type="ISSN">0302-9743</idno><idno type="ISSN">0302-9743</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0302-9743</idno></seriesStmt></fileDesc><profileDesc><textClass><keywords scheme="Teeft" xml:lang="en"><term>Abstract inferences</term><term>Agent paradigm</term><term>Algebra</term><term>Algebra examples</term><term>Available resources</term><term>Backtrack store</term><term>Backtracking</term><term>Backtracking information</term><term>Backtracking purposes</term><term>Broker</term><term>Calculus</term><term>Central proof object</term><term>Centralised approach</term><term>Computer algebra system maple</term><term>Computer algebra systems</term><term>Concrete examples</term><term>Core system</term><term>Current proof context</term><term>Deduction calculus</term><term>Deduction proof object</term><term>Deduction systems</term><term>Description operator</term><term>Domain tactics</term><term>Exible</term><term>Extensionality reasoning</term><term>External reasoners</term><term>External reasoning systems</term><term>External system</term><term>External systems</term><term>Future work</term><term>Graphical user interface loui</term><term>Group theory</term><term>Heterogeneous systems</term><term>Heuristic</term><term>Heuristic criteria</term><term>Interactive</term><term>Knowledge sources</term><term>Large proofs</term><term>Lnai</term><term>Logic broker architecture</term><term>Logical issues</term><term>Loui</term><term>Maple service</term><term>Mathweb</term><term>Model generator</term><term>Natural deduction layer</term><term>Natural deduction proof search</term><term>Natural deduction rules</term><term>Natural deduction style</term><term>Oants</term><term>Open approach</term><term>Partial proof</term><term>Partial proofs</term><term>Partial result</term><term>Partial results</term><term>Particular niches</term><term>Particular parameter instantiations</term><term>Problem classes</term><term>Proc</term><term>Promising direction</term><term>Proof data structure</term><term>Proof object</term><term>Proof search</term><term>Proof step</term><term>Propositional</term><term>Propositional logic prover</term><term>Prover</term><term>Provers</term><term>Reactive</term><term>Reactive layer</term><term>Reactive suggestion layer</term><term>Reactive suggestion mechanism</term><term>Reasoner</term><term>Reasoning</term><term>Reasoning agents</term><term>Reasoning system</term><term>Reasoning systems</term><term>Rstorder clauses</term><term>Search space</term><term>Simple examples</term><term>Skeptical approach</term><term>Skolem variables</term><term>Specialised</term><term>Specialised reasoning systems</term><term>Springer</term><term>Subgoal</term><term>Symbolic computation</term><term>System architecture</term><term>Theorem prover</term><term>Theorem provers</term><term>Transformation tools</term><term>Unique element</term><term>Unit element</term><term>User</term><term>User interaction</term></keywords></textClass><langUsage><language ident="en">en</language></langUsage></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: This paper discusses experiments with an agent oriented approach to automated and interactive reasoning. The approach combines ideas from two subfields of AI (theorem proving/proof planning and multi-agent systems) and makes use of state of the art distribution techniques to decentralise and spread its reasoning agents over the internet. It particularly supports cooperative proofs between reasoning systems which are strong in different application areas, e.g., higher-order and first-order theorem provers and computer algebra systems</div></front></TEI><affiliations><list><country><li>Allemagne</li><li>Royaume-Uni</li></country><region><li>Angleterre</li><li>Midlands de l'Ouest</li><li>Sarre (Land)</li></region><settlement><li>Birmingham</li><li>Sarrebruck</li></settlement><orgName><li>Université de Birmingham</li></orgName></list><tree><country name="Allemagne"><region name="Sarre (Land)"><name sortKey="Benzmuller, Christoph" sort="Benzmuller, Christoph" uniqKey="Benzmuller C" first="Christoph" last="Benzmüller">Christoph Benzmüller</name></region><name sortKey="Benzmuller, Christoph" sort="Benzmuller, Christoph" uniqKey="Benzmuller C" first="Christoph" last="Benzmüller">Christoph Benzmüller</name><name sortKey="Sorge, Volker" sort="Sorge, Volker" uniqKey="Sorge V" first="Volker" last="Sorge">Volker Sorge</name><name sortKey="Sorge, Volker" sort="Sorge, Volker" uniqKey="Sorge V" first="Volker" last="Sorge">Volker Sorge</name></country><country name="Royaume-Uni"><region name="Angleterre"><name sortKey="Kerber, Manfred" sort="Kerber, Manfred" uniqKey="Kerber M" first="Manfred" last="Kerber">Manfred Kerber</name></region><name sortKey="Jamnik, Mateja" sort="Jamnik, Mateja" uniqKey="Jamnik M" first="Mateja" last="Jamnik">Mateja Jamnik</name><name sortKey="Kerber, Manfred" sort="Kerber, Manfred" uniqKey="Kerber M" first="Manfred" last="Kerber">Manfred Kerber</name></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Sarre/explor/MusicSarreV3/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 000C93 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 000C93 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Sarre
|area= MusicSarreV3
|flux= Main
|étape= Exploration
|type= RBID
|clé= ISTEX:A40A289851FC6A763117E357C28D52A49E98E8ED
|texte= Experiments with an Agent-Oriented Reasoning System
}}
| This area was generated with Dilib version V0.6.33. |  |